\begin{tabbing}
Namer($n$; ${\it Id\_list}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\{\=${\it name}$:int\_seg(0; $n$)$\rightarrow$Id$\mid$ \+
\\[0ex]inject(int\_seg(0; $n$); Id; ${\it name}$) $\wedge$ ($\forall$$i$:int\_seg(0; $n$). $\neg$(${\it name}$($i$) $\in$ ${\it Id\_list}$))\} 
\-
\end{tabbing}